E:Type{i}, T, V:(IdIdType{i}), M:(IdLnkIdType{i}), loc:(EId), knd:(EKnd),
val:(e:Eeventtype(knd;loc;V;M;e)), when, after:(x:Ide:ET(loc(e),x)),
sndr:({e:E| isrcv(knd(e)) }E),
Trans:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(x:IdT(i,x))),
Send:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(Msg(M) List)),
Choose:(i,a:Id(x:IdT(i,x))(V(i,a)+Unit)).
ESMachineAxiom(E;T;V;M;loc;knd;val;when;after;sndr;Trans;Send;Choose)  Prop{i'} 

latex

Definitions

False, P  Q, A, t  T, f(a), x:A. B(x), isrcv(k), x:AB(x), x:AB(x), P & Q, P  Q, b, tag(k), lnk(k), b, , s = t, Prop, islocal(k), act(k), Unit, left+right, kindcase(k; a.f(a); l,t.g(l;t) ), eventtype(k;loc;V;M;e), Type, Id, IdLnk, Knd, {x:A| B(x) }, x,y. t(x;y), x. t(x), Msg(M), type List, x.A(x), msg(l;t;v), (x  l), outl(x), isl(x), A & B, ESMachineAxiom(E;T;V;M;loc;knd;val;when;after;sndr;Trans;Send;Choose)

Lemmas

isl wf, outl wf, l member wf, msg wf, unit wf, Msg wf, kindcase wf, eventtype wf, Knd wf, IdLnk wf, Id wf, eqtt to assert, iff transitivity, eqff to assert, actof wf, islocal wf, bool wf, bnot wf, not wf, assert wf, subtype rel self, lnk wf, tagof wf, islocal-not-isrcv, assert of bnot, isrcv wf